
%\paragraph{Dynamic Update in Workflow Applications}


We now illustrate our framework in the context of a simple 
model of a \emph{workflow application}.
To this end, we adapt the example we describe in~\cite{dGP13}.
%where we have shown how adaptable processes are suitable in the workflow setting. 
Our intention is to show an application of the main features of adaptable processes
(notably, explicit locations and update processes) 
and their combination with \emph{delegation}, the well-known instrument to represent 
reconfiguration in session-typed processes.

Briefly, a workflow is a conceptual unit that describes how  a 
number of \emph{activities} coordinate to achieve a particular task.
A workflow-based application usually consists of a \emph{workflow runtime engine} 
that contains a number of workflows running concurrently on top of it; a \emph{workflow base library} on which activities may rely on; and of a number of
 \emph{runtime services}, which are
 application dependent and implement things such as transaction handling and communication with other applications.
 A simple abstraction of a workflow application is the following  process:
 $$
  App \triangleq \componentbig{\nm{wfa}^0}{\, \componentbbig{\nm{we}^0}{\nmu{WE} \parallel \nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k} \parallel \component{\nm{\nm{wbl}}}{0}{}{\nmu{BL}}} \parallel \nmu{S}_{1} \parallel \cdots \parallel \nmu{S}_{j}\,}
% App \midef \component{\nm{wfa}}{\, \component{\nm{we}}{\nmu{WE} \parallel \nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k} \parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \nmu{S}_{1} \parallel \cdots \parallel \nmu{S}_{j}\,}
 $$
 where the application is modeled as an adaptable process \nm{wfa} 
 which contains a workflow engine \nm{we} and a number of 
 runtime services $\nmu{S}_{1}, \ldots, \nmu{S}_{j}$.
In turn,  the workflow engine contains 
a number of workflows $\nm{W}_{1}, \ldots, \nm{W}_{k}$, a
process \nmu{WE} (which represents the engine's behavior and is left unspecified), 
and an adaptable process \nm{wbl} representing the base library (also left unspecified).
As described before, each workflow is composed of a number of activities.
We model each $\nm{W}_{i}$ as an adaptable process $\nm{w}_{i}$
containing 
a process $\nmu{WL}_{i}$
---representing the workflow's logic---, 
and $n$ activities, each of them is formalized as an adaptable process $\nm{a}_{j}$:
%\todo{$ea_1$ stands for execution environment for $a_i$}
%$$
%\nm{W}_{i} = \componentbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n  \component{\nm{a}_j}{0}{}{!\open{c:\rho}.\nmu{P}_{j}}  \,},
%$$
%%%%%%%%% ========================================================= %%%%%%%
$$
\nm{W}_{i} \triangleq \componentbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n  \component{\nm{a}_j}{0}{}{\nmu{P}_{j}}  \,},
$$
In the context of the $i$-th workflow, let us assume the following structure for the first activity:
\begin{eqnarray*}
%C \!\!& \!\!\triangleq \!\!& \nopen{a}{c:\overline{\sigma}}.\outC{c}{u,p}.\branch{c}{n_1{:}Q_1 \parallel n_1{:}Q_2}.\close{c} \\
\nmu{P}_1 \!\!& \!\!\triangleq \!\!& \nopen{a}{s:\sigma}.\inC{s}{u,p}.\select{s}{n_1.Q_1}.\close{s} 
\end{eqnarray*}
where 
$\sigma$ is assumed to capture the session on $s$ (i.e., the input, the selection, 
and the unspecified behavior represented by $Q_1$). % is assumed to realize the behavior .
%and where $R$ represents the platform in which $S$ is deployed.
%$\mathsf{Sys}$ may proceed by establishing a session of type $\sigma$ between $S$ and $C$ (realized by $P_1$ and $Q_1$).
We now illustrate a simple reconfiguration policy for $\component{\nm{a}_1}{0}{}{\nmu{P}_{1}}$, expressible in our language.
To lighten up notation, we will omit sub-indexes, writing simply $\component{\nm{a}}{0}{}{\nmu{P}}$.

Suppose $\nmu{WL}_{i} \triangleq R $, where $R $ is a reconfiguration policy for 
activity $\nm{a}_{}$, defined as follows:
\begin{eqnarray*}
R  & \triangleq &
\ifte{e}{\mupdate{\nm{a} }{\component{\nm{b} }{0}{}{\mathsf{X}}}{\sigma}{\sigma}}
{\mupdate{\nm{a} }{\component{\nm{a'} }{0}{}{\nmu{P'} }  \parallel \component{\nm{a''} }{0}{}{\nmu{P''} } }{\sigma}{\Delta}} \quad\text{where:} \\
\nmu{P'}  \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s:\sigma}.\nopen{b}{d:!(\sigma)}.\throw{d}{s}.\close{d} \\
\nmu{P''}  \!\!& \!\!\triangleq \!\!& \!\!\nopen{b}{e:?(\sigma)}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.Q_1}.\close{s}.\close{e} 
\end{eqnarray*}
%represents a simple adaptation routine enforcing explicit distribution of interacting processes.
Thus, $R $ formalizes a flexible reconfiguration policy that depends on the boolean value $e$ reduces to:
if $e$ reduces to true, then the behavior at activity $\nm{a} $ will be kept unchanged, but it will be relocated to  $\nm{b} $:
$$
\nm{W}_{i} \pired^* \componentbig{\nm{w}_{i}^0}{\, \component{\nm{b}}{0}{}{\nmu{P}}  \parallel \prod_{j=2}^n  \component{\nm{a}_j}{0}{}{\nmu{P}_{j}}  \,},
$$
Otherwise, if $e$ reduces to false, an update action on $\nm{a} $
will 
reconfigure the distributed structure of $\nmu{P} $:
$$
\nm{W}_{i} \pired^* \componentbig{\nm{w}_{i}^0}{\, \component{\nm{a'}}{0}{}{\nmu{P'}}  \parallel \component{\nm{a''}}{0}{}{\nmu{P''}}  \parallel \prod_{j=2}^n  \component{\nm{a}_j}{0}{}{\nmu{P}_{j}}  \,},
$$
Thus, in a single step, 
the monolithic service $\nmu{P} $ will be replaced with a more flexible 
implementation in which $\nmu{P'} $ (located  at $\nm{a'} $) first establishes a session and then \emph{delegates} it to $\nmu{P''} $ (located at $\nm{a''} $).
This update action is transparent to any user of the first activity of $\nm{W}_{i}$; it 
is possible because
the interface of $\nmu{P}_1$ (i.e.,~$\sigma$)  coincides with the annotation of the update process.
Also, observe that interface $\Delta$ contains entries for session types $!(\sigma)$ and $?(\sigma)$,
which are declared in $\nmu{P'} $ and $\nmu{P''} $, respectively.

Clearly, %there are plenty of possibilities for the definition of $R$; 
more involved reconfiguration
policies (in particular, persistent ones) are possible. 
The above scenario already illustrates how
our framework extends the expressiveness of session-typed languages
with located and update processes. % and update actions.
Our type system not only ensures correct communications between $\nmu{P}$ and its partner on $s$:
by relying on Cor.~\ref{cor:cons}, we know that well-typedness also implies
session consistency, i.e., % between $C$ and $S$, i.e., 
an update action on  $\nm{a}$ will not occur if $\nmu{P}$ has already established a session.

%%%%%%%%% ========================================================= %%%%%%%
%\newpage
%the activity $\nm{a}_{j}$ is modeled as a session, and the number of active session represents the users that are currently executing it.  
%One can notice that all the components of the workflow are modeled as adaptable processes, this way the design  is as dynamic and flexible as possible. Indeed, this choice allows to make consistent updates of all the workflow's parts, ensuring, for instance,  that no activity is disrupted by an uncontrolled update. 
%For example, one can imagine of having in parallel to the whole system $App$, a service $S$ that is responsible for the updates. 
%We can imagine several shapes for $S$:
%
%\begin{enumerate}
% \item $S \triangleq \mupdate{\nm{a}_{j}}{\component{\nm{a}_{j}}{0}{}{\mathsf{X}} \parallel \component{\nm{b}}{0}{}{\mathsf{X}}}{\Delta_1}{\Delta_2 }$, where the activity $\nm{a}_{j}$ is replicated in a new activity $\nm{b}$;
% 
% \item  or $S \triangleq \mupdate{\nm{a}_{j}}{\component{\nm{a}_{j}}{0}{}{P'}}{\Delta_1}{\Delta_2 }$ where the activity is completely replaced with a new one and  the types $\Delta_1$ and $\Delta_2$ can be properly set to provide an additional control on the update: i.e. the update can take place only if the conditions posed by $\Delta_1$ are met;
%
%\item by properly combining the two examples above one can obtain more complicate kinds of updates, for instance one can split $\nm{a}_{j}$ into two separate activities maintaining or not the previous behavior.   
%\end{enumerate}
%
%
% 
%
%%\todo{We could enrich this example by treating $P_j$ as we treat $S$ in the previous example:
%%We say that $WL_i$ contains an update action $R$ that may either (i) rename activity $a_j$ (or leave it unchanged in the same location), or (ii) split $a_j$ into two separate activities $a'_j$ and $a''_j$.}
%
%\todo{maybe at the end of section future works-------}
%It is clear that in a workflow activities should not be deadlocked. Being able to statically ensure this property would ease the process of designing functional workflows. Moreover by adding specific constraints on the authorized updates one could model different update policies or protect specific activities.


